\begin{tabbing}
$\forall$\=$T$, $V$:Type, $A$, $B$:($T$$\rightarrow\mathbb{P}$), ${\it dcd\_A}$:($t$:$T$$\rightarrow$Dec($A$($t$))), $f$:(\{$t$:$T$$\mid$ $A$($t$)\} $\rightarrow$$V$), $g$:(\{$t$:$T$$\mid$ $B$($t$)\} $\rightarrow$$V$),\+
\\[0ex]$t$:\{$t$:$T$$\mid$ ($A$($t$)) $\vee$ ($B$($t$))\} .
\-\\[0ex](($A$($t$)) $\Rightarrow$ ([$A$? $f$ : $g$]($t$) = $f$($t$))) \& (($\neg$($A$($t$))) $\Rightarrow$ ([$A$? $f$ : $g$]($t$) = $g$($t$)))
\end{tabbing}